-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(ModularForms/JacobiTheta): derivative of theta function #11824
Conversation
Nice work! |
Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
On my system, compilation of I think merging in the long list of explicit instances would probably be judged as contravening mathlib's "house style" (especially given the conclusion of the recent zulip debate "To automate or not to automate?", where several prominent members of the community argued strongly that we should use automated systems whenever possible and tolerate some slow-down as a result). Other than that, I don't think there's much more that can be done to speed it up. May I suggest that we wait on #11980, and when that is merged, we merge this as it is? |
I tend to agree. It would be good, however, to solve the underlying problem. See also here on Zulip. |
This PR/issue depends on: |
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth. |
Thanks! bors merge |
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
Pull request successfully merged into master. Build succeeded: |
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of `JacobiTheta/TwoVariable.lean`, adding a number of new results needed for Hurwitz and Dirichlet L-series. The main addition is developing the theory of the `z`-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters. We also add a number of new results about the existing `jacobiTheta2` function: - converses of all the convergence statements (showing the series are *never* convergent if tau is outside the upper half-plane), which allows hypotheses to be removed from several results further downstream - differentiability in both variables jointly, not just each variable separately as before.
This is a rewrite of
JacobiTheta/TwoVariable.lean
, adding a number of new results needed for Hurwitz and Dirichlet L-series.The main addition is developing the theory of the
z
-derivative of the theta function, as an object of study in its own right (functional equations, periodicity, holomorphy etc) – this is needed to prove analytic continuation + functional equations for odd Dirichlet characters.We also add a number of new results about the existing
jacobiTheta2
function: